/*
 * ARF.h
 *
 *  Created on:
 *      Author: catching
 */

#ifndef ARF_H
#define ARF_H
#include <set>
#include <map>
#include <stack>
#include <queue>
#include <string>
#include <iostream>
#include "cfa.h"
#include "smt.h"
#include "werePrincessInterface.h"
using namespace std;

extern bool CompareExpr(Expr *e1, Expr *e2);
string itoa(int);


enum TermCheckT{Term, Bad, FakeTrace, FunctionReturn, Others};

/********************************************************
 *ART node
 ********************************************************/

class ART_NODE{
    public:
		Node* cfa_node;//對應的cfa node
		vector<Prop*> predicate;//predicate of the node
		Prop *phi, *cphi;//phi->after abstract, cphi->before abstract
		ART_NODE* Parent;//the parent of this node
		void CLEAR_CHILD();
		void DELETE_CHILD(ART_NODE*);
		ART_NODE* ADD_CHILD(ART_NODE*);
		int nCHILD();//the number of children
		ART_NODE(ART_NODE*, Node*);//constructor. ART_NODE(Parent, 對應的cfa node)
		bool is_traveled();//is this node be traveled?
		bool set_traveled(bool);
		int get_node_id(){return node_id;};
		set<ART_NODE*> CHILD_list;


    private:
		int node_id;
		bool traveled;
};

/*
struct summary_edge{
	string function_name;
	Prop* p;
	set<pair<Prop*, int*> > set_p;
};
*/
/*
struct Prop_c{
	Prop* p2;
	int* count;
	Prop_c(Prop* p, int i){
		count = new int(i);
		p2 = p;
		next = NULL;
	};
	Prop_c* next;
};
*/

class summary_edge{
	public:
		string function_name;
		ART_NODE* root;//which ART produce this summary edge
		ART_NODE* leaf;
		Prop* p1;
		Prop* p2;
		vector<ART_NODE*> call_node;//the nodes that use this summary edge
};

class caller_tree{
	public:
		ART_NODE* caller;
		ART_NODE* root_of_tree;
		Prop* cphi;
		caller_tree(ART_NODE* c, ART_NODE* r, Prop* cp){
			caller = c;
			root_of_tree = r;
			cphi = cp;
			return ;
		}
};

/********************************************************
 *ART forest
 ********************************************************/
class ARF{
    private:
		//bool is_equal(ART*, ART*);//check if two nodes are equal->for two roots of ARTs
		stack<ART_NODE*> processing_node;
		map<string, CFA*> function_map;//the map <function name, CFA>
		vector<summary_edge> summary_edge_set;//the map function and Summary Edge
		//map<ART_NODE*, int> ART_counting;
		map<string, set<ART_NODE*>*> func_to_root;//functions have several ARTs, the map states the ART nodes(the root s of ARTs) belong which functions
		map<string, set<ART_NODE*>*> function_art_map;//the map states which ART node call this function
		//map<ART_NODE*, ART_NODE*> call_to_callee;
		vector<caller_tree> caller_tree_table;
		map<ART_NODE*, ART_NODE*> call_to_return;//which node return to me
		map<ART_NODE*, map<Node*, set<ART_NODE*>*> > cover_map;
		Prop* copy_prop(Prop*);
		Expr* copy_expr(Expr*);
		void del_prop(Prop*);
		void del_expr(Expr*);
		void Remove_from_processing_node(ART_NODE*);
		void Remove_from_Covermap(ART_NODE*);
		void Remove_Descendant(ART_NODE*);
		void Back_Trace(ART_NODE*);
		bool is_Covered(ART_NODE*);
		bool is_Covered(string, ART_NODE*, ART_NODE*);
		bool is_equal(ART_NODE*, ART_NODE*);
		bool is_equal(Prop*, Prop*);
		ART_NODE* get_initial(ART_NODE*);//to the root of ART

		string Func_Belong(ART_NODE*);//return the function name of the ART node

		void Print_ART(ART_NODE* );//function for Graph_out
		void Print_ARFile(ART_NODE* ,ofstream& );//function for Graph_out
		void add_func_predicate(ART_NODE*, vector<VarExpr*>, string);
		void add_cfa_predicate(ART_NODE*);
		Prop* ComputePost_Function(Prop*,vector<Expr*>,vector<VarExpr*>);
		Prop* ComputePost_Assign(Prop *phi, Expr *x, Expr *e);
		Prop* ComputePre_Assign(Prop *phi, Expr *x, Expr *e);
		void Add_Tag_to_Expr(Expr*, int);
		void Add_Tag_to_All_Expr(Node*,Prop*, int);
		void Remove_Tag_of_Expr(Expr*);
		void Remove_Tag_of_All_Expr(Prop*);
		vector<Expr*>* global_var;

    public:
		ARF(vector<CFA>*, vector<Expr*>*);//the constructor of ART forest, start with main function
		//void Ady*);//call a function
		void Graph_out(char*);
		void Graph_out();
		void Print_Summary_edge();
};


#endif
